0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 3 ms)
↳2 CpxWeightedTrs
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxTypedWeightedTrs
↳5 CompletionProof (UPPER BOUND(ID), 0 ms)
↳6 CpxTypedWeightedCompleteTrs
↳7 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳8 CpxRNTS
↳9 CompleteCoflocoProof (⇔, 5751 ms)
↳10 BOUNDS(1, n^2)
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
log(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
minus(x, 0) → x [1]
minus(s(x), s(y)) → minus(x, y) [1]
quot(0, s(y)) → 0 [1]
quot(s(x), s(y)) → s(quot(minus(x, y), s(y))) [1]
le(0, y) → true [1]
le(s(x), 0) → false [1]
le(s(x), s(y)) → le(x, y) [1]
inc(s(x)) → s(inc(x)) [1]
inc(0) → s(0) [1]
log(x) → logIter(x, 0) [1]
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y)) [1]
if(false, b, x, y) → logZeroError [1]
if(true, false, x, s(y)) → y [1]
if(true, true, x, y) → logIter(x, y) [1]
minus(x, 0) → x [1]
minus(s(x), s(y)) → minus(x, y) [1]
quot(0, s(y)) → 0 [1]
quot(s(x), s(y)) → s(quot(minus(x, y), s(y))) [1]
le(0, y) → true [1]
le(s(x), 0) → false [1]
le(s(x), s(y)) → le(x, y) [1]
inc(s(x)) → s(inc(x)) [1]
inc(0) → s(0) [1]
log(x) → logIter(x, 0) [1]
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), quot(x, s(s(0))), inc(y)) [1]
if(false, b, x, y) → logZeroError [1]
if(true, false, x, s(y)) → y [1]
if(true, true, x, y) → logIter(x, y) [1]
| minus :: 0:s:logZeroError → 0:s:logZeroError → 0:s:logZeroError 0 :: 0:s:logZeroError s :: 0:s:logZeroError → 0:s:logZeroError quot :: 0:s:logZeroError → 0:s:logZeroError → 0:s:logZeroError le :: 0:s:logZeroError → 0:s:logZeroError → true:false true :: true:false false :: true:false inc :: 0:s:logZeroError → 0:s:logZeroError log :: 0:s:logZeroError → 0:s:logZeroError logIter :: 0:s:logZeroError → 0:s:logZeroError → 0:s:logZeroError if :: true:false → true:false → 0:s:logZeroError → 0:s:logZeroError → 0:s:logZeroError logZeroError :: 0:s:logZeroError |
minus(v0, v1) → null_minus [0]
quot(v0, v1) → null_quot [0]
le(v0, v1) → null_le [0]
inc(v0) → null_inc [0]
if(v0, v1, v2, v3) → null_if [0]
null_minus, null_quot, null_le, null_inc, null_if
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
0 => 0
true => 2
false => 1
logZeroError => 1
null_minus => 0
null_quot => 0
null_le => 0
null_inc => 0
null_if => 0
if(z, z', z'', z1) -{ 1 }→ y :|: z = 2, x >= 0, y >= 0, z'' = x, z1 = 1 + y, z' = 1
if(z, z', z'', z1) -{ 1 }→ logIter(x, y) :|: z = 2, z1 = y, z' = 2, x >= 0, y >= 0, z'' = x
if(z, z', z'', z1) -{ 1 }→ 1 :|: b >= 0, z1 = y, z = 1, x >= 0, y >= 0, z' = b, z'' = x
if(z, z', z'', z1) -{ 0 }→ 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
inc(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
inc(z) -{ 1 }→ 1 + inc(x) :|: x >= 0, z = 1 + x
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 }→ le(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
le(z, z') -{ 1 }→ 2 :|: y >= 0, z = 0, z' = y
le(z, z') -{ 1 }→ 1 :|: x >= 0, z = 1 + x, z' = 0
le(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
log(z) -{ 1 }→ logIter(x, 0) :|: x >= 0, z = x
logIter(z, z') -{ 1 }→ if(le(1 + 0, x), le(1 + (1 + 0), x), quot(x, 1 + (1 + 0)), inc(y)) :|: x >= 0, y >= 0, z = x, z' = y
minus(z, z') -{ 1 }→ x :|: x >= 0, z = x, z' = 0
minus(z, z') -{ 1 }→ minus(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
minus(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
quot(z, z') -{ 1 }→ 0 :|: z' = 1 + y, y >= 0, z = 0
quot(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
quot(z, z') -{ 1 }→ 1 + quot(minus(x, y), 1 + y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
| eq(start(V, V1, V16, V17),0,[minus(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V16, V17),0,[quot(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V16, V17),0,[le(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V16, V17),0,[inc(V, Out)],[V >= 0]). eq(start(V, V1, V16, V17),0,[log(V, Out)],[V >= 0]). eq(start(V, V1, V16, V17),0,[logIter(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V16, V17),0,[if(V, V1, V16, V17, Out)],[V >= 0,V1 >= 0,V16 >= 0,V17 >= 0]). eq(minus(V, V1, Out),1,[],[Out = V2,V2 >= 0,V = V2,V1 = 0]). eq(minus(V, V1, Out),1,[minus(V3, V4, Ret)],[Out = Ret,V1 = 1 + V4,V3 >= 0,V4 >= 0,V = 1 + V3]). eq(quot(V, V1, Out),1,[],[Out = 0,V1 = 1 + V5,V5 >= 0,V = 0]). eq(quot(V, V1, Out),1,[minus(V6, V7, Ret10),quot(Ret10, 1 + V7, Ret1)],[Out = 1 + Ret1,V1 = 1 + V7,V6 >= 0,V7 >= 0,V = 1 + V6]). eq(le(V, V1, Out),1,[],[Out = 2,V8 >= 0,V = 0,V1 = V8]). eq(le(V, V1, Out),1,[],[Out = 1,V9 >= 0,V = 1 + V9,V1 = 0]). eq(le(V, V1, Out),1,[le(V10, V11, Ret2)],[Out = Ret2,V1 = 1 + V11,V10 >= 0,V11 >= 0,V = 1 + V10]). eq(inc(V, Out),1,[inc(V12, Ret11)],[Out = 1 + Ret11,V12 >= 0,V = 1 + V12]). eq(inc(V, Out),1,[],[Out = 1,V = 0]). eq(log(V, Out),1,[logIter(V13, 0, Ret3)],[Out = Ret3,V13 >= 0,V = V13]). eq(logIter(V, V1, Out),1,[le(1 + 0, V14, Ret0),le(1 + (1 + 0), V14, Ret12),quot(V14, 1 + (1 + 0), Ret21),inc(V15, Ret31),if(Ret0, Ret12, Ret21, Ret31, Ret4)],[Out = Ret4,V14 >= 0,V15 >= 0,V = V14,V1 = V15]). eq(if(V, V1, V16, V17, Out),1,[],[Out = 1,V18 >= 0,V17 = V19,V = 1,V20 >= 0,V19 >= 0,V1 = V18,V16 = V20]). eq(if(V, V1, V16, V17, Out),1,[],[Out = V21,V = 2,V22 >= 0,V21 >= 0,V16 = V22,V17 = 1 + V21,V1 = 1]). eq(if(V, V1, V16, V17, Out),1,[logIter(V23, V24, Ret5)],[Out = Ret5,V = 2,V17 = V24,V1 = 2,V23 >= 0,V24 >= 0,V16 = V23]). eq(minus(V, V1, Out),0,[],[Out = 0,V25 >= 0,V26 >= 0,V = V25,V1 = V26]). eq(quot(V, V1, Out),0,[],[Out = 0,V27 >= 0,V28 >= 0,V = V27,V1 = V28]). eq(le(V, V1, Out),0,[],[Out = 0,V29 >= 0,V30 >= 0,V = V29,V1 = V30]). eq(inc(V, Out),0,[],[Out = 0,V31 >= 0,V = V31]). eq(if(V, V1, V16, V17, Out),0,[],[Out = 0,V17 = V32,V33 >= 0,V16 = V34,V35 >= 0,V = V33,V1 = V35,V34 >= 0,V32 >= 0]). input_output_vars(minus(V,V1,Out),[V,V1],[Out]). input_output_vars(quot(V,V1,Out),[V,V1],[Out]). input_output_vars(le(V,V1,Out),[V,V1],[Out]). input_output_vars(inc(V,Out),[V],[Out]). input_output_vars(log(V,Out),[V],[Out]). input_output_vars(logIter(V,V1,Out),[V,V1],[Out]). input_output_vars(if(V,V1,V16,V17,Out),[V,V1,V16,V17],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. recursive : [inc/2]
1. recursive : [le/3]
2. recursive : [minus/3]
3. recursive : [quot/3]
4. recursive : [if/5,logIter/3]
5. non_recursive : [log/2]
6. non_recursive : [start/4]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into inc/2
1. SCC is partially evaluated into le/3
2. SCC is partially evaluated into minus/3
3. SCC is partially evaluated into quot/3
4. SCC is partially evaluated into logIter/3
5. SCC is completely evaluated into other SCCs
6. SCC is partially evaluated into start/4
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations inc/2
* CE 28 is refined into CE [29]
* CE 27 is refined into CE [30]
* CE 26 is refined into CE [31]
### Cost equations --> "Loop" of inc/2
* CEs [31] --> Loop 19
* CEs [29] --> Loop 20
* CEs [30] --> Loop 21
### Ranking functions of CR inc(V,Out)
* RF of phase [19]: [V]
#### Partial ranking functions of CR inc(V,Out)
* Partial RF of phase [19]:
- RF of loop [19:1]:
V
### Specialization of cost equations le/3
* CE 25 is refined into CE [32]
* CE 23 is refined into CE [33]
* CE 22 is refined into CE [34]
* CE 24 is refined into CE [35]
### Cost equations --> "Loop" of le/3
* CEs [35] --> Loop 22
* CEs [32] --> Loop 23
* CEs [33] --> Loop 24
* CEs [34] --> Loop 25
### Ranking functions of CR le(V,V1,Out)
* RF of phase [22]: [V,V1]
#### Partial ranking functions of CR le(V,V1,Out)
* Partial RF of phase [22]:
- RF of loop [22:1]:
V
V1
### Specialization of cost equations minus/3
* CE 18 is refined into CE [36]
* CE 16 is refined into CE [37]
* CE 17 is refined into CE [38]
### Cost equations --> "Loop" of minus/3
* CEs [38] --> Loop 26
* CEs [36] --> Loop 27
* CEs [37] --> Loop 28
### Ranking functions of CR minus(V,V1,Out)
* RF of phase [26]: [V,V1]
#### Partial ranking functions of CR minus(V,V1,Out)
* Partial RF of phase [26]:
- RF of loop [26:1]:
V
V1
### Specialization of cost equations quot/3
* CE 19 is refined into CE [39]
* CE 21 is refined into CE [40]
* CE 20 is refined into CE [41,42,43]
### Cost equations --> "Loop" of quot/3
* CEs [43] --> Loop 29
* CEs [42] --> Loop 30
* CEs [41] --> Loop 31
* CEs [39,40] --> Loop 32
### Ranking functions of CR quot(V,V1,Out)
* RF of phase [29]: [V-1,V-V1+1]
* RF of phase [31]: [V]
#### Partial ranking functions of CR quot(V,V1,Out)
* Partial RF of phase [29]:
- RF of loop [29:1]:
V-1
V-V1+1
* Partial RF of phase [31]:
- RF of loop [31:1]:
V
### Specialization of cost equations logIter/3
* CE 15 is refined into CE [44,45,46,47,48,49,50,51]
* CE 12 is refined into CE [52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143]
* CE 14 is refined into CE [144,145,146,147,148,149]
* CE 13 is refined into CE [150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165]
### Cost equations --> "Loop" of logIter/3
* CEs [165] --> Loop 33
* CEs [164] --> Loop 34
* CEs [163] --> Loop 35
* CEs [157,161] --> Loop 36
* CEs [156,160] --> Loop 37
* CEs [155,159] --> Loop 38
* CEs [153] --> Loop 39
* CEs [152] --> Loop 40
* CEs [151] --> Loop 41
* CEs [162] --> Loop 42
* CEs [154,158] --> Loop 43
* CEs [150] --> Loop 44
* CEs [64,68,72,76,88,92,96,100,104,108,112,116,128,132,136,140] --> Loop 45
* CEs [146,149] --> Loop 46
* CEs [145,148] --> Loop 47
* CEs [80,81,82,83,84,85,86,87,120,121,122,123,124,125,126,127,144,147] --> Loop 48
* CEs [44,45,46,47,48,49,50,51] --> Loop 49
* CEs [52,53,54,55,56,57,58,59,60,61,62,63,65,66,67,69,70,71,73,74,75,77,78,79,89,90,91,93,94,95,97,98,99,101,102,103,105,106,107,109,110,111,113,114,115,117,118,119,129,130,131,133,134,135,137,138,139,141,142,143] --> Loop 50
### Ranking functions of CR logIter(V,V1,Out)
* RF of phase [33,34,35,36,37,38,42,43]: [V-1]
#### Partial ranking functions of CR logIter(V,V1,Out)
* Partial RF of phase [33,34,35,36,37,38,42,43]:
- RF of loop [33:1,34:1,35:1,42:1]:
V-2
- RF of loop [36:1,37:1,38:1,43:1]:
V-1
- RF of loop [42:1,43:1]:
-V1+1 depends on loops [33:1,35:1,36:1,38:1]
### Specialization of cost equations start/4
* CE 3 is refined into CE [166,167,168,169,170,171,172]
* CE 4 is refined into CE [173]
* CE 2 is refined into CE [174]
* CE 5 is refined into CE [175]
* CE 6 is refined into CE [176,177,178]
* CE 7 is refined into CE [179,180,181,182,183]
* CE 8 is refined into CE [184,185,186,187,188]
* CE 9 is refined into CE [189,190,191,192]
* CE 10 is refined into CE [193,194,195,196,197]
* CE 11 is refined into CE [198,199,200,201,202,203,204]
### Cost equations --> "Loop" of start/4
* CEs [176,185,202] --> Loop 51
* CEs [170] --> Loop 52
* CEs [168,169] --> Loop 53
* CEs [166,167,171,172] --> Loop 54
* CEs [173,179] --> Loop 55
* CEs [200,201] --> Loop 56
* CEs [175] --> Loop 57
* CEs [174,177,178,180,181,182,183,184,186,187,188,189,190,191,192,193,194,195,196,197,198,199,203,204] --> Loop 58
### Ranking functions of CR start(V,V1,V16,V17)
#### Partial ranking functions of CR start(V,V1,V16,V17)
Computing Bounds
=====================================
#### Cost of chains of inc(V,Out):
* Chain [[19],21]: 1*it(19)+1
Such that:it(19) =< Out
with precondition: [V+1=Out,V>=1]
* Chain [[19],20]: 1*it(19)+0
Such that:it(19) =< Out
with precondition: [Out>=1,V>=Out]
* Chain [21]: 1
with precondition: [V=0,Out=1]
* Chain [20]: 0
with precondition: [Out=0,V>=0]
#### Cost of chains of le(V,V1,Out):
* Chain [[22],25]: 1*it(22)+1
Such that:it(22) =< V
with precondition: [Out=2,V>=1,V1>=V]
* Chain [[22],24]: 1*it(22)+1
Such that:it(22) =< V1
with precondition: [Out=1,V1>=1,V>=V1+1]
* Chain [[22],23]: 1*it(22)+0
Such that:it(22) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [25]: 1
with precondition: [V=0,Out=2,V1>=0]
* Chain [24]: 1
with precondition: [V1=0,Out=1,V>=1]
* Chain [23]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of minus(V,V1,Out):
* Chain [[26],28]: 1*it(26)+1
Such that:it(26) =< V1
with precondition: [V=Out+V1,V1>=1,V>=V1]
* Chain [[26],27]: 1*it(26)+0
Such that:it(26) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [28]: 1
with precondition: [V1=0,V=Out,V>=0]
* Chain [27]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of quot(V,V1,Out):
* Chain [[31],32]: 2*it(31)+1
Such that:it(31) =< Out
with precondition: [V1=1,Out>=1,V>=Out]
* Chain [[31],30,32]: 2*it(31)+1*s(3)+2
Such that:s(3) =< 1
it(31) =< Out
with precondition: [V1=1,Out>=2,V>=Out]
* Chain [[29],32]: 2*it(29)+1*s(6)+1
Such that:it(29) =< V-V1+1
aux(3) =< V
it(29) =< aux(3)
s(6) =< aux(3)
with precondition: [V1>=2,Out>=1,V+2>=2*Out+V1]
* Chain [[29],30,32]: 2*it(29)+1*s(3)+1*s(6)+2
Such that:it(29) =< V-V1+1
s(3) =< V1
aux(4) =< V
it(29) =< aux(4)
s(6) =< aux(4)
with precondition: [V1>=2,Out>=2,V+3>=2*Out+V1]
* Chain [32]: 1
with precondition: [Out=0,V>=0,V1>=0]
* Chain [30,32]: 1*s(3)+2
Such that:s(3) =< V1
with precondition: [Out=1,V>=1,V1>=1]
#### Cost of chains of logIter(V,V1,Out):
* Chain [[33,34,35,36,37,38,42,43],50]: 22*it(33)+12*it(35)+7*it(37)+6*it(38)+7*it(42)+7*it(43)+19*s(10)+142*s(11)+48*s(34)+24*s(136)+15*s(361)+3*s(362)+1*s(363)+6*s(368)+1*s(369)+2*s(379)+2*s(387)+9*s(388)+1*s(399)+5*s(400)+3*s(401)+2*s(404)+6
Such that:aux(48) =< 1
aux(49) =< 2
aux(111) =< 2*V-V1
aux(52) =< 2*V+2*V1+2
aux(82) =< 3*V+4*V1
aux(81) =< 3*V+4*V1+2
aux(84) =< V/2+V1
aux(124) =< -V1+1
aux(125) =< V
aux(126) =< 2*V
aux(127) =< 2*V+2*V1
aux(128) =< 3*V
s(136) =< aux(48)
s(34) =< aux(49)
s(11) =< aux(127)
s(10) =< aux(52)
aux(105) =< aux(125)
it(33) =< aux(125)
it(35) =< aux(125)
it(37) =< aux(125)
it(38) =< aux(125)
it(42) =< aux(125)
it(43) =< aux(125)
s(409) =< aux(125)
aux(110) =< aux(126)
it(38) =< aux(126)
it(42) =< aux(126)
it(43) =< aux(126)
aux(108) =< aux(127)
aux(110) =< aux(127)
it(38) =< aux(127)
s(409) =< aux(126)
aux(108) =< aux(128)
aux(110) =< aux(128)
it(35) =< aux(128)
it(42) =< aux(128)
s(409) =< aux(128)
it(37) =< aux(128)
it(38) =< aux(128)
it(43) =< aux(128)
aux(112) =< aux(125)
aux(87) =< aux(84)+1
aux(92) =< aux(84)
it(43) =< aux(110)+aux(108)+aux(108)+aux(127)+aux(111)
s(402) =< aux(110)+aux(108)+aux(108)+aux(127)+aux(111)
s(365) =< aux(125)*2
s(363) =< it(33)*aux(84)
s(364) =< it(33)*aux(125)
aux(105) =< aux(125)+aux(125)+aux(124)
it(42) =< aux(125)+aux(125)+aux(124)
s(409) =< aux(125)+aux(125)+aux(124)
it(43) =< aux(125)+aux(125)+aux(124)
s(390) =< it(37)*aux(87)
s(369) =< it(33)*aux(87)
s(403) =< aux(105)*2
s(402) =< it(42)*aux(112)
s(399) =< aux(105)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(82)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(81)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(382) =< it(35)*aux(92)
s(404) =< s(409)
s(400) =< s(403)
s(388) =< aux(126)
s(401) =< s(402)
s(361) =< s(365)
s(387) =< s(390)
s(379) =< s(382)
s(368) =< aux(128)
s(362) =< s(364)
with precondition: [Out=0,V>=2,V1>=0]
* Chain [[33,34,35,36,37,38,42,43],48]: 22*it(33)+12*it(35)+7*it(37)+6*it(38)+7*it(42)+7*it(43)+15*s(361)+3*s(362)+1*s(363)+6*s(368)+1*s(369)+2*s(379)+11*s(380)+2*s(387)+9*s(388)+1*s(399)+5*s(400)+3*s(401)+2*s(404)+36*s(410)+9*s(422)+7
Such that:aux(147) =< 1
aux(148) =< 2
aux(111) =< 2*V-V1
aux(82) =< 3*V+4*V1
aux(81) =< 3*V+4*V1+2
aux(84) =< V/2+V1
aux(124) =< -V1+1
aux(151) =< V
aux(152) =< 2*V
aux(153) =< 2*V+2*V1
aux(154) =< 3*V
s(422) =< aux(148)
s(380) =< aux(153)
s(410) =< aux(147)
aux(105) =< aux(151)
it(33) =< aux(151)
it(35) =< aux(151)
it(37) =< aux(151)
it(38) =< aux(151)
it(42) =< aux(151)
it(43) =< aux(151)
s(409) =< aux(151)
aux(110) =< aux(152)
it(38) =< aux(152)
it(42) =< aux(152)
it(43) =< aux(152)
aux(108) =< aux(153)
aux(110) =< aux(153)
it(38) =< aux(153)
s(409) =< aux(152)
aux(108) =< aux(154)
aux(110) =< aux(154)
it(35) =< aux(154)
it(42) =< aux(154)
s(409) =< aux(154)
it(37) =< aux(154)
it(38) =< aux(154)
it(43) =< aux(154)
aux(112) =< aux(151)
aux(87) =< aux(84)+1
aux(92) =< aux(84)
it(43) =< aux(110)+aux(108)+aux(108)+aux(153)+aux(111)
s(402) =< aux(110)+aux(108)+aux(108)+aux(153)+aux(111)
s(365) =< aux(151)*2
s(363) =< it(33)*aux(84)
s(364) =< it(33)*aux(151)
aux(105) =< aux(151)+aux(151)+aux(124)
it(42) =< aux(151)+aux(151)+aux(124)
s(409) =< aux(151)+aux(151)+aux(124)
it(43) =< aux(151)+aux(151)+aux(124)
s(390) =< it(37)*aux(87)
s(369) =< it(33)*aux(87)
s(403) =< aux(105)*2
s(402) =< it(42)*aux(112)
s(399) =< aux(105)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(82)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(81)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(382) =< it(35)*aux(92)
s(404) =< s(409)
s(400) =< s(403)
s(388) =< aux(152)
s(401) =< s(402)
s(361) =< s(365)
s(387) =< s(390)
s(379) =< s(382)
s(368) =< aux(154)
s(362) =< s(364)
with precondition: [Out=0,V>=2,V1>=0]
* Chain [[33,34,35,36,37,38,42,43],47]: 22*it(33)+12*it(35)+7*it(37)+6*it(38)+7*it(42)+7*it(43)+15*s(361)+3*s(362)+1*s(363)+6*s(368)+1*s(369)+2*s(379)+3*s(380)+2*s(387)+9*s(388)+1*s(399)+5*s(400)+3*s(401)+2*s(404)+4*s(463)+2*s(465)+1*s(468)+7
Such that:aux(157) =< 1
s(468) =< 2
aux(111) =< 2*V-V1
aux(119) =< 2*V+2*V1
aux(120) =< 2*V+2*V1-2*Out
aux(81) =< 3*V+4*V1+2
aux(82) =< 3*V+4*V1-4*Out
aux(84) =< V/2+V1
aux(124) =< -V1+1
aux(158) =< Out+1
aux(159) =< V
aux(160) =< 2*V
aux(161) =< 3*V
s(465) =< aux(158)
s(463) =< aux(157)
aux(105) =< aux(159)
it(33) =< aux(159)
it(35) =< aux(159)
it(37) =< aux(159)
it(38) =< aux(159)
it(42) =< aux(159)
it(43) =< aux(159)
s(409) =< aux(159)
aux(110) =< aux(160)
it(38) =< aux(160)
it(42) =< aux(160)
it(43) =< aux(160)
aux(107) =< aux(119)
aux(108) =< aux(119)
aux(110) =< aux(119)
it(38) =< aux(119)
aux(107) =< aux(120)
aux(108) =< aux(120)
aux(110) =< aux(120)
it(38) =< aux(120)
s(409) =< aux(160)
aux(108) =< aux(161)
aux(110) =< aux(161)
it(35) =< aux(161)
it(42) =< aux(161)
s(409) =< aux(161)
it(37) =< aux(161)
it(38) =< aux(161)
it(43) =< aux(161)
aux(112) =< aux(159)
aux(87) =< aux(84)+1
aux(92) =< aux(84)
it(43) =< aux(110)+aux(108)+aux(108)+aux(107)+aux(111)
s(402) =< aux(110)+aux(108)+aux(108)+aux(107)+aux(111)
s(365) =< aux(159)*2
s(363) =< it(33)*aux(84)
s(364) =< it(33)*aux(159)
aux(105) =< aux(159)+aux(159)+aux(124)
it(42) =< aux(159)+aux(159)+aux(124)
s(409) =< aux(159)+aux(159)+aux(124)
it(43) =< aux(159)+aux(159)+aux(124)
s(390) =< it(37)*aux(87)
s(369) =< it(33)*aux(87)
s(403) =< aux(105)*2
s(402) =< it(42)*aux(112)
s(399) =< aux(105)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(82)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(81)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(382) =< it(35)*aux(92)
s(404) =< s(409)
s(400) =< s(403)
s(388) =< aux(160)
s(401) =< s(402)
s(361) =< s(365)
s(387) =< s(390)
s(379) =< s(382)
s(380) =< aux(107)
s(368) =< aux(161)
s(362) =< s(364)
with precondition: [V>=2,V1>=0,Out>=1,V+V1>=Out+1]
* Chain [[33,34,35,36,37,38,42,43],46]: 22*it(33)+12*it(35)+7*it(37)+6*it(38)+7*it(42)+7*it(43)+15*s(361)+3*s(362)+1*s(363)+6*s(368)+1*s(369)+2*s(379)+5*s(380)+2*s(387)+9*s(388)+1*s(399)+5*s(400)+3*s(401)+2*s(404)+4*s(470)+1*s(475)+6
Such that:aux(164) =< 1
s(475) =< 2
aux(111) =< 2*V-V1
aux(81) =< 3*V+4*V1+2
aux(82) =< 3*V+4*V1-4*Out
aux(84) =< V/2+V1
aux(124) =< -V1+1
aux(166) =< V
aux(167) =< 2*V
aux(168) =< 2*V+2*V1
aux(169) =< 3*V
s(380) =< aux(168)
s(470) =< aux(164)
aux(105) =< aux(166)
it(33) =< aux(166)
it(35) =< aux(166)
it(37) =< aux(166)
it(38) =< aux(166)
it(42) =< aux(166)
it(43) =< aux(166)
s(409) =< aux(166)
aux(110) =< aux(167)
it(38) =< aux(167)
it(42) =< aux(167)
it(43) =< aux(167)
aux(108) =< aux(168)
aux(110) =< aux(168)
it(38) =< aux(168)
s(409) =< aux(167)
aux(108) =< aux(169)
aux(110) =< aux(169)
it(35) =< aux(169)
it(42) =< aux(169)
s(409) =< aux(169)
it(37) =< aux(169)
it(38) =< aux(169)
it(43) =< aux(169)
aux(112) =< aux(166)
aux(87) =< aux(84)+1
aux(92) =< aux(84)
it(43) =< aux(110)+aux(108)+aux(108)+aux(168)+aux(111)
s(402) =< aux(110)+aux(108)+aux(108)+aux(168)+aux(111)
s(365) =< aux(166)*2
s(363) =< it(33)*aux(84)
s(364) =< it(33)*aux(166)
aux(105) =< aux(166)+aux(166)+aux(124)
it(42) =< aux(166)+aux(166)+aux(124)
s(409) =< aux(166)+aux(166)+aux(124)
it(43) =< aux(166)+aux(166)+aux(124)
s(390) =< it(37)*aux(87)
s(369) =< it(33)*aux(87)
s(403) =< aux(105)*2
s(402) =< it(42)*aux(112)
s(399) =< aux(105)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(82)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(81)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(382) =< it(35)*aux(92)
s(404) =< s(409)
s(400) =< s(403)
s(388) =< aux(167)
s(401) =< s(402)
s(361) =< s(365)
s(387) =< s(390)
s(379) =< s(382)
s(368) =< aux(169)
s(362) =< s(364)
with precondition: [V>=2,V1>=0,Out>=0,V+V1>=Out+2]
* Chain [[33,34,35,36,37,38,42,43],45]: 22*it(33)+12*it(35)+7*it(37)+6*it(38)+7*it(42)+7*it(43)+15*s(361)+3*s(362)+1*s(363)+46*s(368)+1*s(369)+2*s(379)+3*s(380)+2*s(387)+9*s(388)+1*s(399)+5*s(400)+3*s(401)+2*s(404)+16*s(481)+8*s(509)+6
Such that:aux(184) =< 1
aux(185) =< 2
aux(111) =< 2*V-V1
aux(82) =< 3*V+4*V1
aux(81) =< 3*V+4*V1+2
aux(84) =< V/2+V1
aux(124) =< -V1+1
aux(187) =< V
aux(188) =< 2*V
aux(189) =< 2*V+2*V1
aux(190) =< 3*V
s(509) =< aux(184)
s(481) =< aux(185)
s(368) =< aux(190)
aux(105) =< aux(187)
it(33) =< aux(187)
it(35) =< aux(187)
it(37) =< aux(187)
it(38) =< aux(187)
it(42) =< aux(187)
it(43) =< aux(187)
s(409) =< aux(187)
aux(110) =< aux(188)
it(38) =< aux(188)
it(42) =< aux(188)
it(43) =< aux(188)
aux(108) =< aux(189)
aux(110) =< aux(189)
it(38) =< aux(189)
s(409) =< aux(188)
aux(108) =< aux(190)
aux(110) =< aux(190)
it(35) =< aux(190)
it(42) =< aux(190)
s(409) =< aux(190)
it(37) =< aux(190)
it(38) =< aux(190)
it(43) =< aux(190)
aux(112) =< aux(187)
aux(87) =< aux(84)+1
aux(92) =< aux(84)
it(43) =< aux(110)+aux(108)+aux(108)+aux(189)+aux(111)
s(402) =< aux(110)+aux(108)+aux(108)+aux(189)+aux(111)
s(365) =< aux(187)*2
s(363) =< it(33)*aux(84)
s(364) =< it(33)*aux(187)
aux(105) =< aux(187)+aux(187)+aux(124)
it(42) =< aux(187)+aux(187)+aux(124)
s(409) =< aux(187)+aux(187)+aux(124)
it(43) =< aux(187)+aux(187)+aux(124)
s(390) =< it(37)*aux(87)
s(369) =< it(33)*aux(87)
s(403) =< aux(105)*2
s(402) =< it(42)*aux(112)
s(399) =< aux(105)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(82)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(81)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(382) =< it(35)*aux(92)
s(404) =< s(409)
s(400) =< s(403)
s(388) =< aux(188)
s(401) =< s(402)
s(361) =< s(365)
s(387) =< s(390)
s(379) =< s(382)
s(380) =< aux(189)
s(362) =< s(364)
with precondition: [Out=0,V>=2,V1>=0]
* Chain [[33,34,35,36,37,38,42,43],44,50]: 22*it(33)+12*it(35)+7*it(37)+6*it(38)+7*it(42)+7*it(43)+68*s(10)+44*s(11)+15*s(361)+3*s(362)+1*s(363)+6*s(368)+1*s(369)+2*s(379)+3*s(380)+2*s(387)+9*s(388)+1*s(399)+5*s(400)+3*s(401)+2*s(404)+12
Such that:aux(191) =< 1
aux(192) =< 2
aux(111) =< 2*V-V1
aux(82) =< 3*V+4*V1
aux(81) =< 3*V+4*V1+2
aux(84) =< V/2+V1
aux(124) =< -V1+1
aux(193) =< V
aux(194) =< 2*V
aux(195) =< 2*V+2*V1
aux(196) =< 3*V
s(11) =< aux(191)
s(10) =< aux(192)
aux(105) =< aux(193)
it(33) =< aux(193)
it(35) =< aux(193)
it(37) =< aux(193)
it(38) =< aux(193)
it(42) =< aux(193)
it(43) =< aux(193)
s(409) =< aux(193)
aux(110) =< aux(194)
it(38) =< aux(194)
it(42) =< aux(194)
it(43) =< aux(194)
aux(108) =< aux(195)
aux(110) =< aux(195)
it(38) =< aux(195)
s(409) =< aux(194)
aux(108) =< aux(196)
aux(110) =< aux(196)
it(35) =< aux(196)
it(42) =< aux(196)
s(409) =< aux(196)
it(37) =< aux(196)
it(38) =< aux(196)
it(43) =< aux(196)
aux(112) =< aux(193)
aux(87) =< aux(84)+1
aux(92) =< aux(84)
it(43) =< aux(110)+aux(108)+aux(108)+aux(195)+aux(111)
s(402) =< aux(110)+aux(108)+aux(108)+aux(195)+aux(111)
s(365) =< aux(193)*2
s(363) =< it(33)*aux(84)
s(364) =< it(33)*aux(193)
aux(105) =< aux(193)+aux(193)+aux(124)
it(42) =< aux(193)+aux(193)+aux(124)
s(409) =< aux(193)+aux(193)+aux(124)
it(43) =< aux(193)+aux(193)+aux(124)
s(390) =< it(37)*aux(87)
s(369) =< it(33)*aux(87)
s(403) =< aux(105)*2
s(402) =< it(42)*aux(112)
s(399) =< aux(105)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(82)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(81)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(382) =< it(35)*aux(92)
s(404) =< s(409)
s(400) =< s(403)
s(388) =< aux(194)
s(401) =< s(402)
s(361) =< s(365)
s(387) =< s(390)
s(379) =< s(382)
s(380) =< aux(195)
s(368) =< aux(196)
s(362) =< s(364)
with precondition: [Out=0,V>=3,V1>=0]
* Chain [[33,34,35,36,37,38,42,43],44,49]: 22*it(33)+12*it(35)+7*it(37)+6*it(38)+7*it(42)+7*it(43)+15*s(361)+3*s(362)+1*s(363)+6*s(368)+1*s(369)+2*s(379)+3*s(380)+2*s(387)+9*s(388)+1*s(399)+5*s(400)+3*s(401)+2*s(404)+3*s(541)+3*s(542)+12
Such that:aux(199) =< 1
aux(200) =< 2
aux(111) =< 2*V-V1
aux(82) =< 3*V+4*V1
aux(81) =< 3*V+4*V1+2
aux(84) =< V/2+V1
aux(124) =< -V1+1
aux(201) =< V
aux(202) =< 2*V
aux(203) =< 2*V+2*V1
aux(204) =< 3*V
s(541) =< aux(199)
s(542) =< aux(200)
aux(105) =< aux(201)
it(33) =< aux(201)
it(35) =< aux(201)
it(37) =< aux(201)
it(38) =< aux(201)
it(42) =< aux(201)
it(43) =< aux(201)
s(409) =< aux(201)
aux(110) =< aux(202)
it(38) =< aux(202)
it(42) =< aux(202)
it(43) =< aux(202)
aux(108) =< aux(203)
aux(110) =< aux(203)
it(38) =< aux(203)
s(409) =< aux(202)
aux(108) =< aux(204)
aux(110) =< aux(204)
it(35) =< aux(204)
it(42) =< aux(204)
s(409) =< aux(204)
it(37) =< aux(204)
it(38) =< aux(204)
it(43) =< aux(204)
aux(112) =< aux(201)
aux(87) =< aux(84)+1
aux(92) =< aux(84)
it(43) =< aux(110)+aux(108)+aux(108)+aux(203)+aux(111)
s(402) =< aux(110)+aux(108)+aux(108)+aux(203)+aux(111)
s(365) =< aux(201)*2
s(363) =< it(33)*aux(84)
s(364) =< it(33)*aux(201)
aux(105) =< aux(201)+aux(201)+aux(124)
it(42) =< aux(201)+aux(201)+aux(124)
s(409) =< aux(201)+aux(201)+aux(124)
it(43) =< aux(201)+aux(201)+aux(124)
s(390) =< it(37)*aux(87)
s(369) =< it(33)*aux(87)
s(403) =< aux(105)*2
s(402) =< it(42)*aux(112)
s(399) =< aux(105)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(82)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(81)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(382) =< it(35)*aux(92)
s(404) =< s(409)
s(400) =< s(403)
s(388) =< aux(202)
s(401) =< s(402)
s(361) =< s(365)
s(387) =< s(390)
s(379) =< s(382)
s(380) =< aux(203)
s(368) =< aux(204)
s(362) =< s(364)
with precondition: [Out=1,V>=3,V1>=0]
* Chain [[33,34,35,36,37,38,42,43],41,50]: 22*it(33)+12*it(35)+7*it(37)+6*it(38)+7*it(42)+7*it(43)+44*s(10)+49*s(34)+15*s(361)+3*s(362)+1*s(363)+6*s(368)+1*s(369)+2*s(379)+3*s(380)+2*s(387)+9*s(388)+1*s(399)+5*s(400)+3*s(401)+2*s(404)+11
Such that:aux(206) =< 1
aux(207) =< 2
aux(111) =< 2*V-V1
aux(82) =< 3*V+4*V1
aux(81) =< 3*V+4*V1+2
aux(84) =< V/2+V1
aux(124) =< -V1+1
aux(208) =< V
aux(209) =< 2*V
aux(210) =< 2*V+2*V1
aux(211) =< 3*V
s(10) =< aux(206)
s(34) =< aux(207)
aux(105) =< aux(208)
it(33) =< aux(208)
it(35) =< aux(208)
it(37) =< aux(208)
it(38) =< aux(208)
it(42) =< aux(208)
it(43) =< aux(208)
s(409) =< aux(208)
aux(110) =< aux(209)
it(38) =< aux(209)
it(42) =< aux(209)
it(43) =< aux(209)
aux(108) =< aux(210)
aux(110) =< aux(210)
it(38) =< aux(210)
s(409) =< aux(209)
aux(108) =< aux(211)
aux(110) =< aux(211)
it(35) =< aux(211)
it(42) =< aux(211)
s(409) =< aux(211)
it(37) =< aux(211)
it(38) =< aux(211)
it(43) =< aux(211)
aux(112) =< aux(208)
aux(87) =< aux(84)+1
aux(92) =< aux(84)
it(43) =< aux(110)+aux(108)+aux(108)+aux(210)+aux(111)
s(402) =< aux(110)+aux(108)+aux(108)+aux(210)+aux(111)
s(365) =< aux(208)*2
s(363) =< it(33)*aux(84)
s(364) =< it(33)*aux(208)
aux(105) =< aux(208)+aux(208)+aux(124)
it(42) =< aux(208)+aux(208)+aux(124)
s(409) =< aux(208)+aux(208)+aux(124)
it(43) =< aux(208)+aux(208)+aux(124)
s(390) =< it(37)*aux(87)
s(369) =< it(33)*aux(87)
s(403) =< aux(105)*2
s(402) =< it(42)*aux(112)
s(399) =< aux(105)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(82)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(81)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(382) =< it(35)*aux(92)
s(404) =< s(409)
s(400) =< s(403)
s(388) =< aux(209)
s(401) =< s(402)
s(361) =< s(365)
s(387) =< s(390)
s(379) =< s(382)
s(380) =< aux(210)
s(368) =< aux(211)
s(362) =< s(364)
with precondition: [Out=0,V>=3,V1>=0]
* Chain [[33,34,35,36,37,38,42,43],41,49]: 22*it(33)+12*it(35)+7*it(37)+6*it(38)+7*it(42)+7*it(43)+15*s(361)+3*s(362)+1*s(363)+6*s(368)+1*s(369)+2*s(379)+3*s(380)+2*s(387)+9*s(388)+1*s(399)+5*s(400)+3*s(401)+2*s(404)+3*s(543)+1*s(552)+11
Such that:aux(212) =< 1
s(552) =< 2
aux(111) =< 2*V-V1
aux(82) =< 3*V+4*V1
aux(81) =< 3*V+4*V1+2
aux(84) =< V/2+V1
aux(124) =< -V1+1
aux(213) =< V
aux(214) =< 2*V
aux(215) =< 2*V+2*V1
aux(216) =< 3*V
s(543) =< aux(212)
aux(105) =< aux(213)
it(33) =< aux(213)
it(35) =< aux(213)
it(37) =< aux(213)
it(38) =< aux(213)
it(42) =< aux(213)
it(43) =< aux(213)
s(409) =< aux(213)
aux(110) =< aux(214)
it(38) =< aux(214)
it(42) =< aux(214)
it(43) =< aux(214)
aux(108) =< aux(215)
aux(110) =< aux(215)
it(38) =< aux(215)
s(409) =< aux(214)
aux(108) =< aux(216)
aux(110) =< aux(216)
it(35) =< aux(216)
it(42) =< aux(216)
s(409) =< aux(216)
it(37) =< aux(216)
it(38) =< aux(216)
it(43) =< aux(216)
aux(112) =< aux(213)
aux(87) =< aux(84)+1
aux(92) =< aux(84)
it(43) =< aux(110)+aux(108)+aux(108)+aux(215)+aux(111)
s(402) =< aux(110)+aux(108)+aux(108)+aux(215)+aux(111)
s(365) =< aux(213)*2
s(363) =< it(33)*aux(84)
s(364) =< it(33)*aux(213)
aux(105) =< aux(213)+aux(213)+aux(124)
it(42) =< aux(213)+aux(213)+aux(124)
s(409) =< aux(213)+aux(213)+aux(124)
it(43) =< aux(213)+aux(213)+aux(124)
s(390) =< it(37)*aux(87)
s(369) =< it(33)*aux(87)
s(403) =< aux(105)*2
s(402) =< it(42)*aux(112)
s(399) =< aux(105)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(82)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(81)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(382) =< it(35)*aux(92)
s(404) =< s(409)
s(400) =< s(403)
s(388) =< aux(214)
s(401) =< s(402)
s(361) =< s(365)
s(387) =< s(390)
s(379) =< s(382)
s(380) =< aux(215)
s(368) =< aux(216)
s(362) =< s(364)
with precondition: [Out=1,V>=3,V1>=0]
* Chain [[33,34,35,36,37,38,42,43],41,45]: 22*it(33)+12*it(35)+7*it(37)+6*it(38)+7*it(42)+7*it(43)+15*s(361)+3*s(362)+1*s(363)+6*s(368)+1*s(369)+2*s(379)+3*s(380)+2*s(387)+9*s(388)+1*s(399)+5*s(400)+3*s(401)+2*s(404)+17*s(481)+9*s(509)+11
Such that:aux(217) =< 1
aux(218) =< 2
aux(111) =< 2*V-V1
aux(82) =< 3*V+4*V1
aux(81) =< 3*V+4*V1+2
aux(84) =< V/2+V1
aux(124) =< -V1+1
aux(219) =< V
aux(220) =< 2*V
aux(221) =< 2*V+2*V1
aux(222) =< 3*V
s(509) =< aux(217)
s(481) =< aux(218)
aux(105) =< aux(219)
it(33) =< aux(219)
it(35) =< aux(219)
it(37) =< aux(219)
it(38) =< aux(219)
it(42) =< aux(219)
it(43) =< aux(219)
s(409) =< aux(219)
aux(110) =< aux(220)
it(38) =< aux(220)
it(42) =< aux(220)
it(43) =< aux(220)
aux(108) =< aux(221)
aux(110) =< aux(221)
it(38) =< aux(221)
s(409) =< aux(220)
aux(108) =< aux(222)
aux(110) =< aux(222)
it(35) =< aux(222)
it(42) =< aux(222)
s(409) =< aux(222)
it(37) =< aux(222)
it(38) =< aux(222)
it(43) =< aux(222)
aux(112) =< aux(219)
aux(87) =< aux(84)+1
aux(92) =< aux(84)
it(43) =< aux(110)+aux(108)+aux(108)+aux(221)+aux(111)
s(402) =< aux(110)+aux(108)+aux(108)+aux(221)+aux(111)
s(365) =< aux(219)*2
s(363) =< it(33)*aux(84)
s(364) =< it(33)*aux(219)
aux(105) =< aux(219)+aux(219)+aux(124)
it(42) =< aux(219)+aux(219)+aux(124)
s(409) =< aux(219)+aux(219)+aux(124)
it(43) =< aux(219)+aux(219)+aux(124)
s(390) =< it(37)*aux(87)
s(369) =< it(33)*aux(87)
s(403) =< aux(105)*2
s(402) =< it(42)*aux(112)
s(399) =< aux(105)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(82)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(81)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(382) =< it(35)*aux(92)
s(404) =< s(409)
s(400) =< s(403)
s(388) =< aux(220)
s(401) =< s(402)
s(361) =< s(365)
s(387) =< s(390)
s(379) =< s(382)
s(380) =< aux(221)
s(368) =< aux(222)
s(362) =< s(364)
with precondition: [Out=0,V>=3,V1>=0]
* Chain [[33,34,35,36,37,38,42,43],40,50]: 22*it(33)+12*it(35)+7*it(37)+6*it(38)+7*it(42)+7*it(43)+42*s(10)+49*s(34)+25*s(136)+15*s(361)+3*s(362)+1*s(363)+6*s(368)+1*s(369)+2*s(379)+2*s(387)+9*s(388)+1*s(399)+5*s(400)+3*s(401)+2*s(404)+12
Such that:aux(223) =< 1
aux(224) =< 2
aux(111) =< 2*V-V1
aux(82) =< 3*V+4*V1
aux(81) =< 3*V+4*V1+2
aux(84) =< V/2+V1
aux(124) =< -V1+1
aux(226) =< V
aux(227) =< 2*V
aux(228) =< 2*V+2*V1
aux(229) =< 3*V
s(136) =< aux(223)
s(34) =< aux(224)
s(10) =< aux(228)
aux(105) =< aux(226)
it(33) =< aux(226)
it(35) =< aux(226)
it(37) =< aux(226)
it(38) =< aux(226)
it(42) =< aux(226)
it(43) =< aux(226)
s(409) =< aux(226)
aux(110) =< aux(227)
it(38) =< aux(227)
it(42) =< aux(227)
it(43) =< aux(227)
aux(108) =< aux(228)
aux(110) =< aux(228)
it(38) =< aux(228)
s(409) =< aux(227)
aux(108) =< aux(229)
aux(110) =< aux(229)
it(35) =< aux(229)
it(42) =< aux(229)
s(409) =< aux(229)
it(37) =< aux(229)
it(38) =< aux(229)
it(43) =< aux(229)
aux(112) =< aux(226)
aux(87) =< aux(84)+1
aux(92) =< aux(84)
it(43) =< aux(110)+aux(108)+aux(108)+aux(228)+aux(111)
s(402) =< aux(110)+aux(108)+aux(108)+aux(228)+aux(111)
s(365) =< aux(226)*2
s(363) =< it(33)*aux(84)
s(364) =< it(33)*aux(226)
aux(105) =< aux(226)+aux(226)+aux(124)
it(42) =< aux(226)+aux(226)+aux(124)
s(409) =< aux(226)+aux(226)+aux(124)
it(43) =< aux(226)+aux(226)+aux(124)
s(390) =< it(37)*aux(87)
s(369) =< it(33)*aux(87)
s(403) =< aux(105)*2
s(402) =< it(42)*aux(112)
s(399) =< aux(105)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(82)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(81)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(382) =< it(35)*aux(92)
s(404) =< s(409)
s(400) =< s(403)
s(388) =< aux(227)
s(401) =< s(402)
s(361) =< s(365)
s(387) =< s(390)
s(379) =< s(382)
s(368) =< aux(229)
s(362) =< s(364)
with precondition: [Out=0,V>=3,V1>=0]
* Chain [[33,34,35,36,37,38,42,43],40,49]: 22*it(33)+12*it(35)+7*it(37)+6*it(38)+7*it(42)+7*it(43)+15*s(361)+3*s(362)+1*s(363)+6*s(368)+1*s(369)+2*s(379)+8*s(380)+2*s(387)+9*s(388)+1*s(399)+5*s(400)+3*s(401)+2*s(404)+1*s(553)+1*s(554)+12
Such that:s(553) =< 1
s(554) =< 2
aux(111) =< 2*V-V1
aux(82) =< 3*V+4*V1
aux(81) =< 3*V+4*V1+2
aux(84) =< V/2+V1
aux(124) =< -V1+1
aux(231) =< V
aux(232) =< 2*V
aux(233) =< 2*V+2*V1
aux(234) =< 3*V
s(380) =< aux(233)
aux(105) =< aux(231)
it(33) =< aux(231)
it(35) =< aux(231)
it(37) =< aux(231)
it(38) =< aux(231)
it(42) =< aux(231)
it(43) =< aux(231)
s(409) =< aux(231)
aux(110) =< aux(232)
it(38) =< aux(232)
it(42) =< aux(232)
it(43) =< aux(232)
aux(108) =< aux(233)
aux(110) =< aux(233)
it(38) =< aux(233)
s(409) =< aux(232)
aux(108) =< aux(234)
aux(110) =< aux(234)
it(35) =< aux(234)
it(42) =< aux(234)
s(409) =< aux(234)
it(37) =< aux(234)
it(38) =< aux(234)
it(43) =< aux(234)
aux(112) =< aux(231)
aux(87) =< aux(84)+1
aux(92) =< aux(84)
it(43) =< aux(110)+aux(108)+aux(108)+aux(233)+aux(111)
s(402) =< aux(110)+aux(108)+aux(108)+aux(233)+aux(111)
s(365) =< aux(231)*2
s(363) =< it(33)*aux(84)
s(364) =< it(33)*aux(231)
aux(105) =< aux(231)+aux(231)+aux(124)
it(42) =< aux(231)+aux(231)+aux(124)
s(409) =< aux(231)+aux(231)+aux(124)
it(43) =< aux(231)+aux(231)+aux(124)
s(390) =< it(37)*aux(87)
s(369) =< it(33)*aux(87)
s(403) =< aux(105)*2
s(402) =< it(42)*aux(112)
s(399) =< aux(105)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(82)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(81)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(382) =< it(35)*aux(92)
s(404) =< s(409)
s(400) =< s(403)
s(388) =< aux(232)
s(401) =< s(402)
s(361) =< s(365)
s(387) =< s(390)
s(379) =< s(382)
s(368) =< aux(234)
s(362) =< s(364)
with precondition: [Out=1,V>=3,V1>=0]
* Chain [[33,34,35,36,37,38,42,43],39,50]: 22*it(33)+12*it(35)+7*it(37)+6*it(38)+7*it(42)+7*it(43)+42*s(10)+49*s(34)+25*s(136)+15*s(361)+3*s(362)+1*s(363)+6*s(368)+1*s(369)+2*s(379)+2*s(387)+9*s(388)+1*s(399)+5*s(400)+3*s(401)+2*s(404)+11
Such that:aux(235) =< 1
aux(236) =< 2
aux(111) =< 2*V-V1
aux(82) =< 3*V+4*V1
aux(81) =< 3*V+4*V1+2
aux(84) =< V/2+V1
aux(124) =< -V1+1
aux(238) =< V
aux(239) =< 2*V
aux(240) =< 2*V+2*V1
aux(241) =< 3*V
s(136) =< aux(235)
s(34) =< aux(236)
s(10) =< aux(240)
aux(105) =< aux(238)
it(33) =< aux(238)
it(35) =< aux(238)
it(37) =< aux(238)
it(38) =< aux(238)
it(42) =< aux(238)
it(43) =< aux(238)
s(409) =< aux(238)
aux(110) =< aux(239)
it(38) =< aux(239)
it(42) =< aux(239)
it(43) =< aux(239)
aux(108) =< aux(240)
aux(110) =< aux(240)
it(38) =< aux(240)
s(409) =< aux(239)
aux(108) =< aux(241)
aux(110) =< aux(241)
it(35) =< aux(241)
it(42) =< aux(241)
s(409) =< aux(241)
it(37) =< aux(241)
it(38) =< aux(241)
it(43) =< aux(241)
aux(112) =< aux(238)
aux(87) =< aux(84)+1
aux(92) =< aux(84)
it(43) =< aux(110)+aux(108)+aux(108)+aux(240)+aux(111)
s(402) =< aux(110)+aux(108)+aux(108)+aux(240)+aux(111)
s(365) =< aux(238)*2
s(363) =< it(33)*aux(84)
s(364) =< it(33)*aux(238)
aux(105) =< aux(238)+aux(238)+aux(124)
it(42) =< aux(238)+aux(238)+aux(124)
s(409) =< aux(238)+aux(238)+aux(124)
it(43) =< aux(238)+aux(238)+aux(124)
s(390) =< it(37)*aux(87)
s(369) =< it(33)*aux(87)
s(403) =< aux(105)*2
s(402) =< it(42)*aux(112)
s(399) =< aux(105)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(82)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(81)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(382) =< it(35)*aux(92)
s(404) =< s(409)
s(400) =< s(403)
s(388) =< aux(239)
s(401) =< s(402)
s(361) =< s(365)
s(387) =< s(390)
s(379) =< s(382)
s(368) =< aux(241)
s(362) =< s(364)
with precondition: [Out=0,V>=3,V1>=0]
* Chain [[33,34,35,36,37,38,42,43],39,49]: 22*it(33)+12*it(35)+7*it(37)+6*it(38)+7*it(42)+7*it(43)+15*s(361)+3*s(362)+1*s(363)+6*s(368)+1*s(369)+2*s(379)+8*s(380)+2*s(387)+9*s(388)+1*s(399)+5*s(400)+3*s(401)+2*s(404)+1*s(556)+1*s(557)+11
Such that:s(556) =< 1
s(557) =< 2
aux(111) =< 2*V-V1
aux(82) =< 3*V+4*V1
aux(81) =< 3*V+4*V1+2
aux(84) =< V/2+V1
aux(124) =< -V1+1
aux(243) =< V
aux(244) =< 2*V
aux(245) =< 2*V+2*V1
aux(246) =< 3*V
s(380) =< aux(245)
aux(105) =< aux(243)
it(33) =< aux(243)
it(35) =< aux(243)
it(37) =< aux(243)
it(38) =< aux(243)
it(42) =< aux(243)
it(43) =< aux(243)
s(409) =< aux(243)
aux(110) =< aux(244)
it(38) =< aux(244)
it(42) =< aux(244)
it(43) =< aux(244)
aux(108) =< aux(245)
aux(110) =< aux(245)
it(38) =< aux(245)
s(409) =< aux(244)
aux(108) =< aux(246)
aux(110) =< aux(246)
it(35) =< aux(246)
it(42) =< aux(246)
s(409) =< aux(246)
it(37) =< aux(246)
it(38) =< aux(246)
it(43) =< aux(246)
aux(112) =< aux(243)
aux(87) =< aux(84)+1
aux(92) =< aux(84)
it(43) =< aux(110)+aux(108)+aux(108)+aux(245)+aux(111)
s(402) =< aux(110)+aux(108)+aux(108)+aux(245)+aux(111)
s(365) =< aux(243)*2
s(363) =< it(33)*aux(84)
s(364) =< it(33)*aux(243)
aux(105) =< aux(243)+aux(243)+aux(124)
it(42) =< aux(243)+aux(243)+aux(124)
s(409) =< aux(243)+aux(243)+aux(124)
it(43) =< aux(243)+aux(243)+aux(124)
s(390) =< it(37)*aux(87)
s(369) =< it(33)*aux(87)
s(403) =< aux(105)*2
s(402) =< it(42)*aux(112)
s(399) =< aux(105)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(82)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(82)
it(35) =< it(43)+it(42)+it(37)+it(33)+aux(81)
it(38) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(364) =< it(43)+it(42)+it(37)+it(33)+aux(81)
s(382) =< it(35)*aux(92)
s(404) =< s(409)
s(400) =< s(403)
s(388) =< aux(244)
s(401) =< s(402)
s(361) =< s(365)
s(387) =< s(390)
s(379) =< s(382)
s(368) =< aux(246)
s(362) =< s(364)
with precondition: [Out=1,V>=3,V1>=0]
* Chain [50]: 19*s(10)+19*s(11)+120*s(24)+48*s(34)+24*s(136)+6
Such that:aux(48) =< 1
aux(49) =< 2
aux(50) =< V
aux(51) =< V1
aux(52) =< V1+1
s(136) =< aux(48)
s(34) =< aux(49)
s(24) =< aux(50)
s(11) =< aux(51)
s(10) =< aux(52)
with precondition: [Out=0,V>=0,V1>=0]
* Chain [49]: 2*s(543)+2*s(544)+6
Such that:aux(197) =< V1
aux(198) =< V1+1
s(544) =< aux(197)
s(543) =< aux(198)
with precondition: [V=0,Out=1,V1>=0]
* Chain [48]: 36*s(410)+4*s(416)+4*s(419)+9*s(422)+7
Such that:aux(147) =< 1
aux(148) =< 2
aux(149) =< V1
aux(150) =< V1+1
s(422) =< aux(148)
s(419) =< aux(149)
s(416) =< aux(150)
s(410) =< aux(147)
with precondition: [V=1,Out=0,V1>=0]
* Chain [47]: 4*s(463)+2*s(465)+1*s(468)+7
Such that:s(468) =< 2
aux(157) =< 1
aux(158) =< V1+1
s(465) =< aux(158)
s(463) =< aux(157)
with precondition: [V=1,V1=Out,V1>=1]
* Chain [46]: 4*s(470)+2*s(472)+1*s(475)+6
Such that:s(475) =< 2
aux(164) =< 1
aux(165) =< V1
s(472) =< aux(165)
s(470) =< aux(164)
with precondition: [V=1,Out>=0,V1>=Out+1]
* Chain [45]: 40*s(477)+16*s(481)+8*s(509)+6
Such that:aux(184) =< 1
aux(185) =< 2
aux(186) =< V
s(509) =< aux(184)
s(481) =< aux(185)
s(477) =< aux(186)
with precondition: [V1=0,Out=0,V>=0]
* Chain [44,50]: 68*s(10)+44*s(11)+12
Such that:aux(191) =< 1
aux(192) =< 2
s(11) =< aux(191)
s(10) =< aux(192)
with precondition: [V1=0,Out=0,V>=2]
* Chain [44,49]: 3*s(541)+3*s(542)+12
Such that:aux(199) =< 1
aux(200) =< 2
s(541) =< aux(199)
s(542) =< aux(200)
with precondition: [V1=0,Out=1,V>=2]
* Chain [41,50]: 44*s(10)+49*s(34)+11
Such that:aux(206) =< 1
aux(207) =< 2
s(10) =< aux(206)
s(34) =< aux(207)
with precondition: [Out=0,V>=2,V1>=0]
* Chain [41,49]: 3*s(543)+1*s(552)+11
Such that:s(552) =< 2
aux(212) =< 1
s(543) =< aux(212)
with precondition: [Out=1,V>=2,V1>=0]
* Chain [41,45]: 17*s(481)+9*s(509)+11
Such that:aux(217) =< 1
aux(218) =< 2
s(509) =< aux(217)
s(481) =< aux(218)
with precondition: [Out=0,V>=2,V1>=0]
* Chain [40,50]: 19*s(10)+20*s(11)+49*s(34)+25*s(136)+12
Such that:aux(52) =< V1+2
aux(223) =< 1
aux(224) =< 2
aux(225) =< V1+1
s(136) =< aux(223)
s(34) =< aux(224)
s(11) =< aux(225)
s(10) =< aux(52)
with precondition: [Out=0,V>=2,V1>=1]
* Chain [40,49]: 2*s(543)+3*s(544)+1*s(553)+1*s(554)+12
Such that:s(553) =< 1
s(554) =< 2
aux(198) =< V1+2
aux(230) =< V1+1
s(544) =< aux(230)
s(543) =< aux(198)
with precondition: [Out=1,V>=2,V1>=1]
* Chain [39,50]: 19*s(10)+20*s(11)+49*s(34)+25*s(136)+11
Such that:aux(52) =< V1+1
aux(235) =< 1
aux(236) =< 2
aux(237) =< V1
s(136) =< aux(235)
s(34) =< aux(236)
s(11) =< aux(237)
s(10) =< aux(52)
with precondition: [Out=0,V>=2,V1>=1]
* Chain [39,49]: 2*s(543)+3*s(544)+1*s(556)+1*s(557)+11
Such that:s(556) =< 1
s(557) =< 2
aux(198) =< V1+1
aux(242) =< V1
s(544) =< aux(242)
s(543) =< aux(198)
with precondition: [Out=1,V>=2,V1>=1]
#### Cost of chains of start(V,V1,V16,V17):
* Chain [58]: 54*s(1215)+4*s(1218)+900*s(1220)+1*s(1228)+925*s(1233)+1185*s(1250)+528*s(1254)+156*s(1256)+196*s(1257)+78*s(1258)+98*s(1259)+91*s(1260)+14*s(1269)+14*s(1272)+14*s(1274)+28*s(1276)+70*s(1277)+39*s(1279)+420*s(1280)+28*s(1281)+26*s(1282)+248*s(1283)+39*s(1284)+21*s(1285)+12*s(1348)+6*s(1349)+7*s(1350)+3*s(1357)+2*s(1358)+3*s(1359)+3*s(1360)+69*s(1408)+276*s(1429)+156*s(1431)+78*s(1433)+98*s(1434)+91*s(1435)+14*s(1444)+14*s(1447)+14*s(1449)+28*s(1451)+70*s(1452)+39*s(1454)+28*s(1456)+26*s(1457)+39*s(1459)+21*s(1460)+21*s(1461)+12*s(1517)+6*s(1518)+7*s(1519)+3*s(1526)+2*s(1527)+3*s(1528)+3*s(1529)+13
Such that:s(1228) =< V+1
aux(288) =< 1
aux(289) =< 2
aux(290) =< V
aux(291) =< V-V1+1
aux(292) =< 2*V
aux(293) =< 2*V+2
aux(294) =< 2*V-V1
aux(295) =< 2*V+2*V1
aux(296) =< 2*V+2*V1+2
aux(297) =< 3*V
aux(298) =< 3*V+2
aux(299) =< 3*V+4*V1
aux(300) =< 3*V+4*V1+2
aux(301) =< V/2
aux(302) =< V/2+V1
aux(303) =< -V1+1
aux(304) =< V1
aux(305) =< V1+1
aux(306) =< V1+2
s(1250) =< aux(289)
s(1220) =< aux(290)
s(1218) =< aux(291)
s(1215) =< aux(304)
s(1233) =< aux(288)
s(1408) =< aux(305)
s(1429) =< aux(295)
s(1430) =< aux(290)
s(1431) =< aux(290)
s(1257) =< aux(290)
s(1433) =< aux(290)
s(1434) =< aux(290)
s(1435) =< aux(290)
s(1436) =< aux(290)
s(1437) =< aux(292)
s(1433) =< aux(292)
s(1434) =< aux(292)
s(1435) =< aux(292)
s(1438) =< aux(295)
s(1437) =< aux(295)
s(1433) =< aux(295)
s(1436) =< aux(292)
s(1438) =< aux(297)
s(1437) =< aux(297)
s(1431) =< aux(297)
s(1434) =< aux(297)
s(1436) =< aux(297)
s(1257) =< aux(297)
s(1433) =< aux(297)
s(1435) =< aux(297)
s(1264) =< aux(290)
s(1440) =< aux(302)+1
s(1441) =< aux(302)
s(1435) =< s(1437)+s(1438)+s(1438)+aux(295)+aux(294)
s(1442) =< s(1437)+s(1438)+s(1438)+aux(295)+aux(294)
s(1268) =< aux(290)*2
s(1444) =< s(1220)*aux(302)
s(1445) =< s(1220)*aux(290)
s(1430) =< aux(290)+aux(290)+aux(303)
s(1434) =< aux(290)+aux(290)+aux(303)
s(1436) =< aux(290)+aux(290)+aux(303)
s(1435) =< aux(290)+aux(290)+aux(303)
s(1446) =< s(1257)*s(1440)
s(1447) =< s(1220)*s(1440)
s(1448) =< s(1430)*2
s(1442) =< s(1434)*s(1264)
s(1449) =< s(1430)
s(1431) =< s(1435)+s(1434)+s(1257)+s(1220)+aux(299)
s(1433) =< s(1435)+s(1434)+s(1257)+s(1220)+aux(299)
s(1445) =< s(1435)+s(1434)+s(1257)+s(1220)+aux(299)
s(1431) =< s(1435)+s(1434)+s(1257)+s(1220)+aux(300)
s(1433) =< s(1435)+s(1434)+s(1257)+s(1220)+aux(300)
s(1445) =< s(1435)+s(1434)+s(1257)+s(1220)+aux(300)
s(1450) =< s(1431)*s(1441)
s(1451) =< s(1436)
s(1452) =< s(1448)
s(1254) =< aux(292)
s(1454) =< s(1442)
s(1280) =< s(1268)
s(1456) =< s(1446)
s(1457) =< s(1450)
s(1283) =< aux(297)
s(1459) =< s(1445)
s(1460) =< aux(296)
s(1461) =< aux(306)
s(1517) =< aux(290)
s(1518) =< aux(290)
s(1519) =< aux(290)
s(1520) =< aux(292)
s(1518) =< aux(292)
s(1519) =< aux(292)
s(1521) =< aux(295)
s(1522) =< aux(295)
s(1520) =< aux(295)
s(1518) =< aux(295)
s(1521) =< aux(296)
s(1522) =< aux(296)
s(1520) =< aux(296)
s(1518) =< aux(296)
s(1522) =< aux(297)
s(1520) =< aux(297)
s(1517) =< aux(297)
s(1518) =< aux(297)
s(1519) =< aux(297)
s(1519) =< s(1520)+s(1522)+s(1522)+s(1521)+aux(294)
s(1523) =< s(1520)+s(1522)+s(1522)+s(1521)+aux(294)
s(1524) =< s(1220)*aux(290)
s(1519) =< aux(290)+aux(290)+aux(303)
s(1523) =< s(1434)*s(1264)
s(1517) =< s(1519)+s(1434)+s(1257)+s(1220)+aux(299)
s(1518) =< s(1519)+s(1434)+s(1257)+s(1220)+aux(299)
s(1524) =< s(1519)+s(1434)+s(1257)+s(1220)+aux(299)
s(1517) =< s(1519)+s(1434)+s(1257)+s(1220)+aux(300)
s(1518) =< s(1519)+s(1434)+s(1257)+s(1220)+aux(300)
s(1524) =< s(1519)+s(1434)+s(1257)+s(1220)+aux(300)
s(1525) =< s(1517)*s(1441)
s(1526) =< s(1523)
s(1527) =< s(1525)
s(1528) =< s(1521)
s(1529) =< s(1524)
s(1255) =< aux(290)
s(1256) =< aux(290)
s(1258) =< aux(290)
s(1259) =< aux(290)
s(1260) =< aux(290)
s(1261) =< aux(290)
s(1262) =< aux(292)
s(1258) =< aux(292)
s(1259) =< aux(292)
s(1260) =< aux(292)
s(1261) =< aux(292)
s(1262) =< aux(297)
s(1256) =< aux(297)
s(1259) =< aux(297)
s(1261) =< aux(297)
s(1258) =< aux(297)
s(1260) =< aux(297)
s(1265) =< aux(301)+1
s(1266) =< aux(301)
s(1260) =< s(1262)+s(1262)+s(1262)+aux(292)+aux(292)
s(1267) =< s(1262)+s(1262)+s(1262)+aux(292)+aux(292)
s(1269) =< s(1220)*aux(301)
s(1270) =< s(1220)*aux(290)
s(1255) =< aux(290)+aux(290)+aux(288)
s(1259) =< aux(290)+aux(290)+aux(288)
s(1261) =< aux(290)+aux(290)+aux(288)
s(1260) =< aux(290)+aux(290)+aux(288)
s(1271) =< s(1257)*s(1265)
s(1272) =< s(1220)*s(1265)
s(1273) =< s(1255)*2
s(1267) =< s(1259)*s(1264)
s(1274) =< s(1255)
s(1256) =< s(1260)+s(1259)+s(1257)+s(1220)+aux(297)
s(1258) =< s(1260)+s(1259)+s(1257)+s(1220)+aux(297)
s(1270) =< s(1260)+s(1259)+s(1257)+s(1220)+aux(297)
s(1256) =< s(1260)+s(1259)+s(1257)+s(1220)+aux(298)
s(1258) =< s(1260)+s(1259)+s(1257)+s(1220)+aux(298)
s(1270) =< s(1260)+s(1259)+s(1257)+s(1220)+aux(298)
s(1275) =< s(1256)*s(1266)
s(1276) =< s(1261)
s(1277) =< s(1273)
s(1279) =< s(1267)
s(1281) =< s(1271)
s(1282) =< s(1275)
s(1284) =< s(1270)
s(1218) =< aux(290)
s(1285) =< aux(293)
s(1348) =< aux(290)
s(1349) =< aux(290)
s(1350) =< aux(290)
s(1351) =< aux(292)
s(1349) =< aux(292)
s(1350) =< aux(292)
s(1352) =< aux(292)
s(1352) =< aux(293)
s(1351) =< aux(293)
s(1349) =< aux(293)
s(1351) =< aux(297)
s(1348) =< aux(297)
s(1349) =< aux(297)
s(1350) =< aux(297)
s(1350) =< s(1351)+s(1351)+s(1351)+s(1352)+aux(292)
s(1354) =< s(1351)+s(1351)+s(1351)+s(1352)+aux(292)
s(1355) =< s(1220)*aux(290)
s(1350) =< aux(290)+aux(290)+aux(288)
s(1354) =< s(1259)*s(1264)
s(1348) =< s(1350)+s(1259)+s(1257)+s(1220)+aux(297)
s(1349) =< s(1350)+s(1259)+s(1257)+s(1220)+aux(297)
s(1355) =< s(1350)+s(1259)+s(1257)+s(1220)+aux(297)
s(1348) =< s(1350)+s(1259)+s(1257)+s(1220)+aux(298)
s(1349) =< s(1350)+s(1259)+s(1257)+s(1220)+aux(298)
s(1355) =< s(1350)+s(1259)+s(1257)+s(1220)+aux(298)
s(1356) =< s(1348)*s(1266)
s(1357) =< s(1354)
s(1358) =< s(1356)
s(1359) =< s(1352)
s(1360) =< s(1355)
with precondition: [V>=0]
* Chain [57]: 1
with precondition: [V=1,V1>=0,V16>=0,V17>=0]
* Chain [56]: 2*s(1574)+2*s(1577)+8*s(1578)+2*s(1582)+7
Such that:s(1581) =< V1
s(1576) =< V1+1
aux(307) =< 1
aux(308) =< 2
s(1574) =< aux(308)
s(1577) =< s(1576)
s(1578) =< aux(307)
s(1582) =< s(1581)
with precondition: [V=1,V1>=1]
* Chain [55]: 1*s(1584)+4*s(1586)+2
Such that:s(1584) =< 1
s(1585) =< V
s(1586) =< s(1585)
with precondition: [V1=1,V>=1]
* Chain [54]: 48*s(1589)+69*s(1590)+402*s(1606)+540*s(1607)+428*s(1610)+276*s(1611)+156*s(1613)+98*s(1614)+78*s(1615)+98*s(1616)+91*s(1617)+14*s(1626)+14*s(1629)+14*s(1631)+28*s(1633)+70*s(1634)+126*s(1635)+39*s(1636)+210*s(1637)+28*s(1638)+26*s(1639)+124*s(1640)+39*s(1641)+21*s(1642)+21*s(1643)+12*s(1699)+6*s(1700)+7*s(1701)+3*s(1708)+2*s(1709)+3*s(1710)+3*s(1711)+13
Such that:aux(311) =< 1
aux(312) =< 2
aux(313) =< V16
aux(314) =< 2*V16
aux(315) =< 2*V16-V17
aux(316) =< 2*V16+2*V17
aux(317) =< 2*V16+2*V17+2
aux(318) =< 3*V16
aux(319) =< 3*V16+4*V17
aux(320) =< 3*V16+4*V17+2
aux(321) =< V16/2+V17
aux(322) =< -V17+1
aux(323) =< V17
aux(324) =< V17+1
aux(325) =< V17+2
s(1607) =< aux(312)
s(1606) =< aux(311)
s(1589) =< aux(323)
s(1590) =< aux(324)
s(1610) =< aux(313)
s(1611) =< aux(316)
s(1612) =< aux(313)
s(1613) =< aux(313)
s(1614) =< aux(313)
s(1615) =< aux(313)
s(1616) =< aux(313)
s(1617) =< aux(313)
s(1618) =< aux(313)
s(1619) =< aux(314)
s(1615) =< aux(314)
s(1616) =< aux(314)
s(1617) =< aux(314)
s(1620) =< aux(316)
s(1619) =< aux(316)
s(1615) =< aux(316)
s(1618) =< aux(314)
s(1620) =< aux(318)
s(1619) =< aux(318)
s(1613) =< aux(318)
s(1616) =< aux(318)
s(1618) =< aux(318)
s(1614) =< aux(318)
s(1615) =< aux(318)
s(1617) =< aux(318)
s(1621) =< aux(313)
s(1622) =< aux(321)+1
s(1623) =< aux(321)
s(1617) =< s(1619)+s(1620)+s(1620)+aux(316)+aux(315)
s(1624) =< s(1619)+s(1620)+s(1620)+aux(316)+aux(315)
s(1625) =< aux(313)*2
s(1626) =< s(1610)*aux(321)
s(1627) =< s(1610)*aux(313)
s(1612) =< aux(313)+aux(313)+aux(322)
s(1616) =< aux(313)+aux(313)+aux(322)
s(1618) =< aux(313)+aux(313)+aux(322)
s(1617) =< aux(313)+aux(313)+aux(322)
s(1628) =< s(1614)*s(1622)
s(1629) =< s(1610)*s(1622)
s(1630) =< s(1612)*2
s(1624) =< s(1616)*s(1621)
s(1631) =< s(1612)
s(1613) =< s(1617)+s(1616)+s(1614)+s(1610)+aux(319)
s(1615) =< s(1617)+s(1616)+s(1614)+s(1610)+aux(319)
s(1627) =< s(1617)+s(1616)+s(1614)+s(1610)+aux(319)
s(1613) =< s(1617)+s(1616)+s(1614)+s(1610)+aux(320)
s(1615) =< s(1617)+s(1616)+s(1614)+s(1610)+aux(320)
s(1627) =< s(1617)+s(1616)+s(1614)+s(1610)+aux(320)
s(1632) =< s(1613)*s(1623)
s(1633) =< s(1618)
s(1634) =< s(1630)
s(1635) =< aux(314)
s(1636) =< s(1624)
s(1637) =< s(1625)
s(1638) =< s(1628)
s(1639) =< s(1632)
s(1640) =< aux(318)
s(1641) =< s(1627)
s(1642) =< aux(317)
s(1643) =< aux(325)
s(1699) =< aux(313)
s(1700) =< aux(313)
s(1701) =< aux(313)
s(1702) =< aux(314)
s(1700) =< aux(314)
s(1701) =< aux(314)
s(1703) =< aux(316)
s(1704) =< aux(316)
s(1702) =< aux(316)
s(1700) =< aux(316)
s(1703) =< aux(317)
s(1704) =< aux(317)
s(1702) =< aux(317)
s(1700) =< aux(317)
s(1704) =< aux(318)
s(1702) =< aux(318)
s(1699) =< aux(318)
s(1700) =< aux(318)
s(1701) =< aux(318)
s(1701) =< s(1702)+s(1704)+s(1704)+s(1703)+aux(315)
s(1705) =< s(1702)+s(1704)+s(1704)+s(1703)+aux(315)
s(1706) =< s(1610)*aux(313)
s(1701) =< aux(313)+aux(313)+aux(322)
s(1705) =< s(1616)*s(1621)
s(1699) =< s(1701)+s(1616)+s(1614)+s(1610)+aux(319)
s(1700) =< s(1701)+s(1616)+s(1614)+s(1610)+aux(319)
s(1706) =< s(1701)+s(1616)+s(1614)+s(1610)+aux(319)
s(1699) =< s(1701)+s(1616)+s(1614)+s(1610)+aux(320)
s(1700) =< s(1701)+s(1616)+s(1614)+s(1610)+aux(320)
s(1706) =< s(1701)+s(1616)+s(1614)+s(1610)+aux(320)
s(1707) =< s(1699)*s(1623)
s(1708) =< s(1705)
s(1709) =< s(1707)
s(1710) =< s(1703)
s(1711) =< s(1706)
with precondition: [V=2,V1=2,V16>=0,V17>=0]
* Chain [53]: 2*s(1756)+2*s(1759)+8*s(1760)+2*s(1764)+8
Such that:s(1763) =< V17
s(1758) =< V17+1
aux(326) =< 1
aux(327) =< 2
s(1756) =< aux(327)
s(1759) =< s(1758)
s(1760) =< aux(326)
s(1764) =< s(1763)
with precondition: [V=2,V1=2,V16=1,V17>=1]
* Chain [52]: 52*s(1769)+84*s(1770)+40*s(1771)+13
Such that:s(1767) =< 1
s(1768) =< 2
s(1766) =< V16
s(1769) =< s(1767)
s(1770) =< s(1768)
s(1771) =< s(1766)
with precondition: [V=2,V1=2,V17=0,V16>=0]
* Chain [51]: 52*s(1775)+84*s(1776)+40*s(1777)+12
Such that:s(1773) =< 1
s(1774) =< 2
s(1772) =< V
s(1775) =< s(1773)
s(1776) =< s(1774)
s(1777) =< s(1772)
with precondition: [V1=0,V>=0]
Closed-form bounds of start(V,V1,V16,V17):
-------------------------------------
* Chain [58] with precondition: [V>=0]
- Upper bound: 3616*V+3308+nat(V1)*54+1566*V+870*V+ (V+1)+nat(V1+1)*69+nat(V1+2)*21+ (42*V+42)+nat(2*V+2*V1)*405+nat(3*V+4*V1)*42+nat(2*V+2*V1+2)*21+nat(V-V1+1)*4+nat(V/2+V1)*84*V+nat(2*V-V1)*42+42*V*V
- Complexity: n^2
* Chain [57] with precondition: [V=1,V1>=0,V16>=0,V17>=0]
- Upper bound: 1
- Complexity: constant
* Chain [56] with precondition: [V=1,V1>=1]
- Upper bound: 4*V1+21
- Complexity: n
* Chain [55] with precondition: [V1=1,V>=1]
- Upper bound: 4*V+3
- Complexity: n
* Chain [54] with precondition: [V=2,V1=2,V16>=0,V17>=0]
- Upper bound: 3472*V16+1158*V17+1648+ (42*V16+84*V17)*V16+nat(2*V16-V17)*42
- Complexity: n^2
* Chain [53] with precondition: [V=2,V1=2,V16=1,V17>=1]
- Upper bound: 4*V17+22
- Complexity: n
* Chain [52] with precondition: [V=2,V1=2,V17=0,V16>=0]
- Upper bound: 40*V16+233
- Complexity: n
* Chain [51] with precondition: [V1=0,V>=0]
- Upper bound: 40*V+232
- Complexity: n
### Maximum cost of start(V,V1,V16,V17): max([max([max([nat(V1)*2+18+nat(V1+1)*2,nat(V17)*2+19+nat(V17+1)*2]),nat(V16)*1746+1262+nat(V17)*48+nat(2*V16)*168+nat(3*V16)*124+nat(V17+1)*69+nat(V17+2)*21+nat(2*V16+2*V17)*405+nat(3*V16+4*V17)*42+nat(2*V16+2*V17+2)*21+nat(V16/2+V17)*84*nat(V16)+nat(2*V16-V17)*42+ (nat(V16)*40+232)]),3576*V+3076+nat(V1)*54+1566*V+870*V+ (V+1)+nat(V1+1)*69+nat(V1+2)*21+ (42*V+42)+nat(2*V+2*V1)*405+nat(3*V+4*V1)*42+nat(2*V+2*V1+2)*21+nat(V-V1+1)*4+nat(V/2+V1)*84*V+nat(2*V-V1)*42+42*V*V+ (36*V+229)+ (4*V+2)])+1
Asymptotic class: n^2
* Total analysis performed in 5061 ms.